simple functional queue from Okasaki by c-cube · Pull Request #558 · leanprover/cslib

c-cube · 2026-05-11T01:55:12Z

Hi, this is my first attempt at contributing Lean code.

I dug out the old Okasaki, and started off with the simple queue. This should
contain a correctness proof, a complexity proof, and a mapping to a ghost list
of elements. TimeM doesn't seem to be enough for amortized complexity so
I added a module for that, and I also removed the ZeroAdd typeclass constraint
because \N doesn't implement it(!).

AI disclosure: all code is mine, but I had some assistance from GLM 5.1 to
tidy up proof terms and get unstuck.

c-cube · 2026-05-29T02:53:35Z

this is ready for re-review

eric-wieser · 2026-06-05T07:35:22Z

+class Op α o where
+  applyOp : α → o → TimeM ℕ α


This has no docstring; and this only makse sense if you are saying "for any given pair of types α o, there is exactly one possible operation".

how else should I write this? no typeclass at all?

Yes, I think drop the typeclass entirely.

eric-wieser · 2026-06-05T07:39:35Z

+/-- Enqueue an element. -/
+def push {α : Type u} (x : α) (q : FunctionalQueue α)
+    : TimeM ℕ (FunctionalQueue α) := do
+  TimeM.tick 1
+  rebalance ⟨ q.front, x :: q.back ⟩


In my opinion, the TimeM stuff clutters the API here; especially if you find yourself wanting to execute this code, and now end up computing a bunch of counters that you have no interest in. I'd suggest something like

Suggested change

/-- Enqueue an element. -/

def push {α : Type u} (x : α) (q : FunctionalQueue α)

: TimeM ℕ (FunctionalQueue α) := do

TimeM.tick 1

rebalance ⟨ q.front, x :: q.back ⟩

/-- Enqueue an element. -/

def push {α : Type u} (x : α) (q : FunctionalQueue α) : FunctionalQueue α :=

rebalance ⟨q.front, x :: q.back⟩

/-- Push as an algorithm

def pushAlg {α : Type u} (x : α) (q : FunctionalQueue α)

: TimeM ℕ (FunctionalQueue α) := do

TimeM.tick 1

rebalanceAlg ⟨ q.front, x :: q.back ⟩

@[simp] theorem run_pushAlg : (pushAlg x q).ret = pushAlg x q := sorry

and similar for the others.

Perhaps this needs discussion on Zulip.

…e queue

eric-wieser · 2026-06-06T02:18:14Z

+  back : List α
+
+/-- Well-formedness: if front is empty, back must be empty too. -/
+def invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=


Suggested change

def invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=

def Invariant {α : Type u} (q : Raw.FunctionalQueue α) : Prop :=

since this is a Prop

eric-wieser · 2026-06-06T02:18:47Z

+  TimeM.tick 1
+  rebalance ⟨ q.front, x :: q.back ⟩
+
+theorem pushInvariant {α : Type u} (x : α) (q : FunctionalQueue α)


This should be called Invariant.push

eric-wieser · 2026-06-06T02:20:00Z

+/-- Physicist method: a potential (lower bound on savings) defined on a
+    data structure.
+    [Okasaki, *Purely Functional Data Structures*, 1996][okasaki1996] -/
+class Potential (φ α : Type*) [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ] where


Note that you can change this to

Suggested change

class Potential (φ α : Type*) [CommRing φ] [LinearOrder φ] [IsStrictOrderedRing φ] where

class Potential (φ α : Type*) where

c-cube requested review from chenson2018 and fmontesi as code owners May 11, 2026 01:55

c-cube force-pushed the c-cube/functionalQueue branch from b7c4a9c to a3c0424 Compare May 11, 2026 02:50

sorrachai reviewed May 16, 2026

View reviewed changes

Comment thread Cslib/Algorithms/Lean/FunctionalQueue/FunctionalQueue.lean

sorrachai reviewed May 16, 2026

View reviewed changes